package fst.binding

trait Binding {
  type AlsoNominal[T] = T with Nominal[T] // avoid F-bounds

  // something that contains names
  trait Nominal[Self] { 
    // return this entity after swapping a and b
    def swap(a: Name, b: Name): AlsoNominal[Self]

    // a is in the set of free variables of this entity
    def fresh(a: Name): Boolean
    
    def alphaEq(other: AlsoNominal[Self]): Boolean
  }
  
  object Name {
    private[Name] var nextTag: Int = -1 // only for toString
    def apply(name: String) = new Name(name)
    def apply(name: Name) = new Name(name.name)
  }
  class Name(val name: String) extends Nominal[Name] {
    def swap(a: Name, b: Name) : AlsoNominal[Name]
      = if(this.alphaEq(a)) b else if(this.alphaEq(b)) a else this

    def fresh(a: Name) = ! this.alphaEq(a)  

    def alphaEq(other: AlsoNominal[Name]) = other eq this // identity

    override def toString() = name+"$"+tag
    val tag = {Name.nextTag += 1; Name.nextTag} // only used in toString
  }
  
  object \\ {
    def apply[T](x: Name, b: AlsoNominal[T]) = new \\(x, b)
    def unapply[T](abs: \\[T]): Some[(Name, AlsoNominal[T])] = Some(abs.unabs)
  }
  class \\[T](private val binder: Name,
              private val body: AlsoNominal[T]) extends Nominal[\\[T]] {
    def swap(a: Name, b: Name) 
      = new \\(binder swap(a, b), body swap(a, b))

    def fresh(a: Name) 
      = if(a.alphaEq(binder)) true  // implicitly alpha-convert binder
        else body.fresh(a)

    def alphaEq(o: AlsoNominal[\\[T]]): Boolean = (binder.alphaEq(o.binder) && body.alphaEq(o.body)) || 
        ((!binder.alphaEq(o.binder)) && 
         o.body.fresh(binder) && o.body.swap(o.binder, binder).alphaEq(body))

    def unabs: (Name, AlsoNominal[T]) = {
      val freshBinder = Name(binder.name)    // = Name.apply(binder.name) (see object Name)
      (freshBinder, body.swap(binder, freshBinder))
    }
    
    override def toString() = {
      val (x, b) = unabs
      x+" \\\\ "+b
    }
    
  }  
}